DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2022.30

Proofs for Propositional Model Counting

Authors: Johannes K. Fichte, Markus Hecher, and Valentin Roland

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract

Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed. As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.

Cite as

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Proofs for Propositional Model Counting. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.SAT.2022.30,
  author =	{Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
  title =	{{Proofs for Propositional Model Counting}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{30:1--30:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.30},
  URN =		{urn:nbn:de:0030-drops-167043},
  doi =		{10.4230/LIPIcs.SAT.2022.30},
  annote =	{Keywords: Model Counting, Verification, Certified Counting}
}

Document

DOI: 10.4230/LIPIcs.CP.2021.24

Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

Authors: Johannes K. Fichte, Markus Hecher, and Valentin Roland

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract

Propositional model counting (MC) and its extensions as well as applications in the area of probabilistic reasoning have received renewed attention in recent years. As a result, also the need for quickly solving counting-based problems with automated solvers is critical for certain areas. In this paper, we present experiments evaluating various techniques in order to improve the performance of parallel model counting on general purpose graphics processing units (GPGPUs). Thereby, we mainly consider engineering efficient algorithms for model counting on GPGPUs that utilize the treewidth of a propositional formula by means of dynamic programming. The combination of our techniques results in the solver GPUSAT3, which is based on the programming framework Cuda that -compared to other frameworks- shows superior extensibility and driver support. When combining all findings of this work, we show that GPUSAT3 not only solves more instances of the recent Model Counting Competition 2020 (MCC 2020) than existing GPGPU-based systems, but also solves those significantly faster. A portfolio with one of the best solvers of MCC 2020 and GPUSAT3 solves 19% more instances than the former alone in less than half of the runtime.

Cite as

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.CP.2021.24,
  author =	{Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
  title =	{{Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.24},
  URN =		{urn:nbn:de:0030-drops-153150},
  doi =		{10.4230/LIPIcs.CP.2021.24},
  annote =	{Keywords: Propositional Satisfiability, GPGPU, Model Counting, Treewidth, Tree Decomposition}
}

Search Results

Documents authored by Roland, Valentin

Proofs for Propositional Model Counting

Abstract

Cite as

Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

Abstract

Cite as

Thanks for your feedback!

Could not send message